YES 10.057 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule Main
  ((ceiling :: Ratio Int  ->  Int) :: Ratio Int  ->  Int)

module Main where
  import qualified Prelude



Lambda Reductions:
The following Lambda expression
\(_,r)→r

is transformed to
r0 (_,r) = r

The following Lambda expression
\(n,_)→n

is transformed to
n0 (n,_) = n

The following Lambda expression
\(_,r)→r

is transformed to
r1 (_,r) = r

The following Lambda expression
\(q,_)→q

is transformed to
q1 (q,_) = q



↳ HASKELL
  ↳ LR
HASKELL
      ↳ IFR

mainModule Main
  ((ceiling :: Ratio Int  ->  Int) :: Ratio Int  ->  Int)

module Main where
  import qualified Prelude



If Reductions:
The following If expression
if r > 0 then n + 1 else n

is transformed to
ceiling0 True = n + 1
ceiling0 False = n

The following If expression
if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to
primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0 x y False = Zero

The following If expression
if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x

is transformed to
primModNatS0 x y True = primModNatS (primMinusNatS x y) (Succ y)
primModNatS0 x y False = Succ x



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
HASKELL
          ↳ BR

mainModule Main
  ((ceiling :: Ratio Int  ->  Int) :: Ratio Int  ->  Int)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
frac@(Double vz wu)

is replaced by the following term
Double vz wu

The bind variable of the following binding Pattern
frac@(Float wx wy)

is replaced by the following term
Float wx wy



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
HASKELL
              ↳ COR

mainModule Main
  ((ceiling :: Ratio Int  ->  Int) :: Ratio Int  ->  Int)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
HASKELL
                  ↳ LetRed

mainModule Main
  ((ceiling :: Ratio Int  ->  Int) :: Ratio Int  ->  Int)

module Main where
  import qualified Prelude



Let/Where Reductions:
The bindings of the following Let/Where expression
ceiling0 (r > 0)
where 
ceiling0 True = n + 1
ceiling0 False = n
n  = n0 vu8
n0 (n,vw) = n
r  = r0 vu8
r0 (vv,r) = r
vu8  = properFraction x

are unpacked to the following functions on top level
ceilingN xx = ceilingN0 xx (ceilingVu8 xx)

ceilingR0 xx (vv,r) = r

ceilingR xx = ceilingR0 xx (ceilingVu8 xx)

ceilingVu8 xx = properFraction xx

ceilingN0 xx (n,vw) = n

ceilingCeiling0 xx True = ceilingN xx + 1
ceilingCeiling0 xx False = ceilingN xx

The bindings of the following Let/Where expression
(fromIntegral q,r :% y)
where 
q  = q1 vu30
q1 (q,xu) = q
r  = r1 vu30
r1 (xv,r) = r
vu30  = quotRem x y

are unpacked to the following functions on top level
properFractionR1 xy xz (xv,r) = r

properFractionQ1 xy xz (q,xu) = q

properFractionQ xy xz = properFractionQ1 xy xz (properFractionVu30 xy xz)

properFractionR xy xz = properFractionR1 xy xz (properFractionVu30 xy xz)

properFractionVu30 xy xz = quotRem xy xz



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
HASKELL
                      ↳ NumRed

mainModule Main
  ((ceiling :: Ratio Int  ->  Int) :: Ratio Int  ->  Int)

module Main where
  import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
HASKELL
                          ↳ Narrow

mainModule Main
  (ceiling :: Ratio Int  ->  Int)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yu930)) → new_primMulNat(yu930)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yu8000), Succ(yu20900)) → new_primPlusNat(yu8000, yu20900)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(Succ(yu8000), Succ(yu20900)) → new_primMinusNat(yu8000, yu20900)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNatS(Succ(yu2340), Succ(yu2350)) → new_primMinusNatS(yu2340, yu2350)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ DependencyGraphProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS00(yu234, yu235, Zero, Zero) → new_primModNatS02(yu234, yu235)
new_primModNatS01(yu30000000) → new_primModNatS1(yu30000000, Zero)
new_primModNatS2(Succ(yu1960), Zero) → new_primModNatS01(yu1960)
new_primModNatS00(yu234, yu235, Succ(yu2360), Succ(yu2370)) → new_primModNatS00(yu234, yu235, yu2360, yu2370)
new_primModNatS2(Succ(yu1960), Succ(yu1970)) → new_primModNatS00(yu1960, yu1970, yu1960, yu1970)
new_primModNatS02(yu234, yu235) → new_primModNatS(new_primMinusNatS0(yu234, yu235), Succ(yu235))
new_primModNatS0(Succ(yu1960), Succ(yu1970)) → new_primModNatS00(yu1960, yu1970, yu1960, yu1970)
new_primModNatS(Succ(yu8000), yu8100) → new_primModNatS0(yu8000, yu8100)
new_primModNatS0(Succ(yu1960), Zero) → new_primModNatS01(yu1960)
new_primModNatS1(Succ(yu1960), Succ(yu1970)) → new_primModNatS00(yu1960, yu1970, yu1960, yu1970)
new_primModNatS1(Succ(yu1960), Zero) → new_primModNatS01(yu1960)
new_primModNatS00(yu234, yu235, Succ(yu2360), Zero) → new_primModNatS(new_primMinusNatS0(yu234, yu235), Succ(yu235))

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu2350)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu2340), Succ(yu2350)) → new_primMinusNatS0(yu2340, yu2350)
new_primMinusNatS0(Succ(yu2340), Zero) → Succ(yu2340)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 4 less nodes.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
QDP
                                      ↳ UsableRulesProof
                                    ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS01(yu30000000) → new_primModNatS1(yu30000000, Zero)
new_primModNatS1(Succ(yu1960), Zero) → new_primModNatS01(yu1960)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu2350)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu2340), Succ(yu2350)) → new_primMinusNatS0(yu2340, yu2350)
new_primMinusNatS0(Succ(yu2340), Zero) → Succ(yu2340)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                      ↳ UsableRulesProof
QDP
                                          ↳ QReductionProof
                                    ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS01(yu30000000) → new_primModNatS1(yu30000000, Zero)
new_primModNatS1(Succ(yu1960), Zero) → new_primModNatS01(yu1960)

R is empty.
The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                      ↳ UsableRulesProof
                                        ↳ QDP
                                          ↳ QReductionProof
QDP
                                              ↳ QDPSizeChangeProof
                                    ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS01(yu30000000) → new_primModNatS1(yu30000000, Zero)
new_primModNatS1(Succ(yu1960), Zero) → new_primModNatS01(yu1960)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
QDP
                                      ↳ QDPOrderProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS00(yu234, yu235, Zero, Zero) → new_primModNatS02(yu234, yu235)
new_primModNatS00(yu234, yu235, Succ(yu2360), Succ(yu2370)) → new_primModNatS00(yu234, yu235, yu2360, yu2370)
new_primModNatS02(yu234, yu235) → new_primModNatS(new_primMinusNatS0(yu234, yu235), Succ(yu235))
new_primModNatS0(Succ(yu1960), Succ(yu1970)) → new_primModNatS00(yu1960, yu1970, yu1960, yu1970)
new_primModNatS(Succ(yu8000), yu8100) → new_primModNatS0(yu8000, yu8100)
new_primModNatS00(yu234, yu235, Succ(yu2360), Zero) → new_primModNatS(new_primMinusNatS0(yu234, yu235), Succ(yu235))

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu2350)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu2340), Succ(yu2350)) → new_primMinusNatS0(yu2340, yu2350)
new_primMinusNatS0(Succ(yu2340), Zero) → Succ(yu2340)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


new_primModNatS0(Succ(yu1960), Succ(yu1970)) → new_primModNatS00(yu1960, yu1970, yu1960, yu1970)
The remaining pairs can at least be oriented weakly.

new_primModNatS00(yu234, yu235, Zero, Zero) → new_primModNatS02(yu234, yu235)
new_primModNatS00(yu234, yu235, Succ(yu2360), Succ(yu2370)) → new_primModNatS00(yu234, yu235, yu2360, yu2370)
new_primModNatS02(yu234, yu235) → new_primModNatS(new_primMinusNatS0(yu234, yu235), Succ(yu235))
new_primModNatS(Succ(yu8000), yu8100) → new_primModNatS0(yu8000, yu8100)
new_primModNatS00(yu234, yu235, Succ(yu2360), Zero) → new_primModNatS(new_primMinusNatS0(yu234, yu235), Succ(yu235))
Used ordering: Polynomial interpretation [25]:

POL(Succ(x1)) = 1 + x1   
POL(Zero) = 0   
POL(new_primMinusNatS0(x1, x2)) = x1   
POL(new_primModNatS(x1, x2)) = x1   
POL(new_primModNatS0(x1, x2)) = 1 + x1   
POL(new_primModNatS00(x1, x2, x3, x4)) = x1   
POL(new_primModNatS02(x1, x2)) = x1   

The following usable rules [17] were oriented:

new_primMinusNatS0(Succ(yu2340), Succ(yu2350)) → new_primMinusNatS0(yu2340, yu2350)
new_primMinusNatS0(Zero, Succ(yu2350)) → Zero
new_primMinusNatS0(Succ(yu2340), Zero) → Succ(yu2340)
new_primMinusNatS0(Zero, Zero) → Zero



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ QDPOrderProof
QDP
                                          ↳ DependencyGraphProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS00(yu234, yu235, Zero, Zero) → new_primModNatS02(yu234, yu235)
new_primModNatS00(yu234, yu235, Succ(yu2360), Succ(yu2370)) → new_primModNatS00(yu234, yu235, yu2360, yu2370)
new_primModNatS02(yu234, yu235) → new_primModNatS(new_primMinusNatS0(yu234, yu235), Succ(yu235))
new_primModNatS(Succ(yu8000), yu8100) → new_primModNatS0(yu8000, yu8100)
new_primModNatS00(yu234, yu235, Succ(yu2360), Zero) → new_primModNatS(new_primMinusNatS0(yu234, yu235), Succ(yu235))

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu2350)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu2340), Succ(yu2350)) → new_primMinusNatS0(yu2340, yu2350)
new_primMinusNatS0(Succ(yu2340), Zero) → Succ(yu2340)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 4 less nodes.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ QDPOrderProof
                                        ↳ QDP
                                          ↳ DependencyGraphProof
QDP
                                              ↳ UsableRulesProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS00(yu234, yu235, Succ(yu2360), Succ(yu2370)) → new_primModNatS00(yu234, yu235, yu2360, yu2370)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu2350)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu2340), Succ(yu2350)) → new_primMinusNatS0(yu2340, yu2350)
new_primMinusNatS0(Succ(yu2340), Zero) → Succ(yu2340)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ QDPOrderProof
                                        ↳ QDP
                                          ↳ DependencyGraphProof
                                            ↳ QDP
                                              ↳ UsableRulesProof
QDP
                                                  ↳ QReductionProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS00(yu234, yu235, Succ(yu2360), Succ(yu2370)) → new_primModNatS00(yu234, yu235, yu2360, yu2370)

R is empty.
The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ QDPOrderProof
                                        ↳ QDP
                                          ↳ DependencyGraphProof
                                            ↳ QDP
                                              ↳ UsableRulesProof
                                                ↳ QDP
                                                  ↳ QReductionProof
QDP
                                                      ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS00(yu234, yu235, Succ(yu2360), Succ(yu2370)) → new_primModNatS00(yu234, yu235, yu2360, yu2370)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ DependencyGraphProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(yu254, yu255, Zero, Zero) → new_primDivNatS00(yu254, yu255)
new_primDivNatS00(yu254, yu255) → new_primDivNatS(new_primMinusNatS0(Succ(yu254), Succ(yu255)), Succ(yu255))
new_primDivNatS0(yu254, yu255, Succ(yu2560), Succ(yu2570)) → new_primDivNatS0(yu254, yu255, yu2560, yu2570)
new_primDivNatS(Succ(Succ(yu80000)), Succ(yu81000)) → new_primDivNatS0(yu80000, yu81000, yu80000, yu81000)
new_primDivNatS0(yu254, yu255, Succ(yu2560), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(yu254), Succ(yu255)), Succ(yu255))
new_primDivNatS(Succ(Succ(yu80000)), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(yu80000), Zero), Zero)
new_primDivNatS(Succ(Zero), Zero) → new_primDivNatS01
new_primDivNatS01new_primDivNatS(Zero, Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu2350)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu2340), Succ(yu2350)) → new_primMinusNatS0(yu2340, yu2350)
new_primMinusNatS0(Succ(yu2340), Zero) → Succ(yu2340)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 2 less nodes.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
QDP
                                      ↳ UsableRulesProof
                                    ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(yu80000)), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(yu80000), Zero), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu2350)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu2340), Succ(yu2350)) → new_primMinusNatS0(yu2340, yu2350)
new_primMinusNatS0(Succ(yu2340), Zero) → Succ(yu2340)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                      ↳ UsableRulesProof
QDP
                                          ↳ RuleRemovalProof
                                    ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(yu80000)), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(yu80000), Zero), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(Succ(yu2340), Zero) → Succ(yu2340)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

new_primDivNatS(Succ(Succ(yu80000)), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(yu80000), Zero), Zero)

Strictly oriented rules of the TRS R:

new_primMinusNatS0(Succ(yu2340), Zero) → Succ(yu2340)

Used ordering: POLO with Polynomial interpretation [25]:

POL(Succ(x1)) = 2 + 2·x1   
POL(Zero) = 0   
POL(new_primDivNatS(x1, x2)) = x1 + x2   
POL(new_primMinusNatS0(x1, x2)) = 1 + 2·x1 + x2   



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                      ↳ UsableRulesProof
                                        ↳ QDP
                                          ↳ RuleRemovalProof
QDP
                                              ↳ PisEmptyProof
                                    ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
P is empty.
R is empty.
The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
QDP
                                      ↳ Rewriting
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS00(yu254, yu255) → new_primDivNatS(new_primMinusNatS0(Succ(yu254), Succ(yu255)), Succ(yu255))
new_primDivNatS0(yu254, yu255, Zero, Zero) → new_primDivNatS00(yu254, yu255)
new_primDivNatS0(yu254, yu255, Succ(yu2560), Succ(yu2570)) → new_primDivNatS0(yu254, yu255, yu2560, yu2570)
new_primDivNatS(Succ(Succ(yu80000)), Succ(yu81000)) → new_primDivNatS0(yu80000, yu81000, yu80000, yu81000)
new_primDivNatS0(yu254, yu255, Succ(yu2560), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(yu254), Succ(yu255)), Succ(yu255))

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu2350)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu2340), Succ(yu2350)) → new_primMinusNatS0(yu2340, yu2350)
new_primMinusNatS0(Succ(yu2340), Zero) → Succ(yu2340)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primDivNatS00(yu254, yu255) → new_primDivNatS(new_primMinusNatS0(Succ(yu254), Succ(yu255)), Succ(yu255)) at position [0] we obtained the following new rules:

new_primDivNatS00(yu254, yu255) → new_primDivNatS(new_primMinusNatS0(yu254, yu255), Succ(yu255))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ Rewriting
QDP
                                          ↳ Rewriting
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(yu254, yu255, Zero, Zero) → new_primDivNatS00(yu254, yu255)
new_primDivNatS00(yu254, yu255) → new_primDivNatS(new_primMinusNatS0(yu254, yu255), Succ(yu255))
new_primDivNatS(Succ(Succ(yu80000)), Succ(yu81000)) → new_primDivNatS0(yu80000, yu81000, yu80000, yu81000)
new_primDivNatS0(yu254, yu255, Succ(yu2560), Succ(yu2570)) → new_primDivNatS0(yu254, yu255, yu2560, yu2570)
new_primDivNatS0(yu254, yu255, Succ(yu2560), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(yu254), Succ(yu255)), Succ(yu255))

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu2350)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu2340), Succ(yu2350)) → new_primMinusNatS0(yu2340, yu2350)
new_primMinusNatS0(Succ(yu2340), Zero) → Succ(yu2340)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primDivNatS0(yu254, yu255, Succ(yu2560), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(yu254), Succ(yu255)), Succ(yu255)) at position [0] we obtained the following new rules:

new_primDivNatS0(yu254, yu255, Succ(yu2560), Zero) → new_primDivNatS(new_primMinusNatS0(yu254, yu255), Succ(yu255))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
QDP
                                              ↳ QDPOrderProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(yu254, yu255, Zero, Zero) → new_primDivNatS00(yu254, yu255)
new_primDivNatS0(yu254, yu255, Succ(yu2560), Succ(yu2570)) → new_primDivNatS0(yu254, yu255, yu2560, yu2570)
new_primDivNatS(Succ(Succ(yu80000)), Succ(yu81000)) → new_primDivNatS0(yu80000, yu81000, yu80000, yu81000)
new_primDivNatS00(yu254, yu255) → new_primDivNatS(new_primMinusNatS0(yu254, yu255), Succ(yu255))
new_primDivNatS0(yu254, yu255, Succ(yu2560), Zero) → new_primDivNatS(new_primMinusNatS0(yu254, yu255), Succ(yu255))

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu2350)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu2340), Succ(yu2350)) → new_primMinusNatS0(yu2340, yu2350)
new_primMinusNatS0(Succ(yu2340), Zero) → Succ(yu2340)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


new_primDivNatS(Succ(Succ(yu80000)), Succ(yu81000)) → new_primDivNatS0(yu80000, yu81000, yu80000, yu81000)
The remaining pairs can at least be oriented weakly.

new_primDivNatS0(yu254, yu255, Zero, Zero) → new_primDivNatS00(yu254, yu255)
new_primDivNatS0(yu254, yu255, Succ(yu2560), Succ(yu2570)) → new_primDivNatS0(yu254, yu255, yu2560, yu2570)
new_primDivNatS00(yu254, yu255) → new_primDivNatS(new_primMinusNatS0(yu254, yu255), Succ(yu255))
new_primDivNatS0(yu254, yu255, Succ(yu2560), Zero) → new_primDivNatS(new_primMinusNatS0(yu254, yu255), Succ(yu255))
Used ordering: Polynomial interpretation [25]:

POL(Succ(x1)) = 1 + x1   
POL(Zero) = 0   
POL(new_primDivNatS(x1, x2)) = x1   
POL(new_primDivNatS0(x1, x2, x3, x4)) = x1   
POL(new_primDivNatS00(x1, x2)) = x1   
POL(new_primMinusNatS0(x1, x2)) = x1   

The following usable rules [17] were oriented:

new_primMinusNatS0(Succ(yu2340), Zero) → Succ(yu2340)
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Zero, Succ(yu2350)) → Zero
new_primMinusNatS0(Succ(yu2340), Succ(yu2350)) → new_primMinusNatS0(yu2340, yu2350)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ QDPOrderProof
QDP
                                                  ↳ DependencyGraphProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(yu254, yu255, Zero, Zero) → new_primDivNatS00(yu254, yu255)
new_primDivNatS00(yu254, yu255) → new_primDivNatS(new_primMinusNatS0(yu254, yu255), Succ(yu255))
new_primDivNatS0(yu254, yu255, Succ(yu2560), Succ(yu2570)) → new_primDivNatS0(yu254, yu255, yu2560, yu2570)
new_primDivNatS0(yu254, yu255, Succ(yu2560), Zero) → new_primDivNatS(new_primMinusNatS0(yu254, yu255), Succ(yu255))

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu2350)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu2340), Succ(yu2350)) → new_primMinusNatS0(yu2340, yu2350)
new_primMinusNatS0(Succ(yu2340), Zero) → Succ(yu2340)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ QDPOrderProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
QDP
                                                      ↳ UsableRulesProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(yu254, yu255, Succ(yu2560), Succ(yu2570)) → new_primDivNatS0(yu254, yu255, yu2560, yu2570)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(yu2350)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(yu2340), Succ(yu2350)) → new_primMinusNatS0(yu2340, yu2350)
new_primMinusNatS0(Succ(yu2340), Zero) → Succ(yu2340)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ QDPOrderProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ QDP
                                                      ↳ UsableRulesProof
QDP
                                                          ↳ QReductionProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(yu254, yu255, Succ(yu2560), Succ(yu2570)) → new_primDivNatS0(yu254, yu255, yu2560, yu2570)

R is empty.
The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ AND
                                    ↳ QDP
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ QDPOrderProof
                                                ↳ QDP
                                                  ↳ DependencyGraphProof
                                                    ↳ QDP
                                                      ↳ UsableRulesProof
                                                        ↳ QDP
                                                          ↳ QReductionProof
QDP
                                                              ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(yu254, yu255, Succ(yu2560), Succ(yu2570)) → new_primDivNatS0(yu254, yu255, yu2560, yu2570)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_ceilingCeiling0(yu30000000, Succ(yu19900), Succ(yu10500)) → new_ceilingCeiling0(yu30000000, yu19900, yu10500)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_ceilingCeiling00(yu30000000, Succ(yu13200), Succ(yu19300)) → new_ceilingCeiling00(yu30000000, yu13200, yu19300)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: